Nuprl Lemma : preserved_by_symmetric
4,23
postcript
pdf
T
:Type,
P
:(
T
Prop),
R
:(
T
T
Prop). (Sym
x
,
y
:
T
.
x
R
y
)
R
preserves
P
R
^-1 preserves
P
latex
Definitions
Sym
x
,
y
:
T
.
E
(
x
;
y
)
,
R
^-1
,
R
preserves
P
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
f
y
,
Prop
,
t
T
origin
T:Type, P:(T
Prop), R:(TTProp). (Sym x,y:T. x R y) 
R preserves P R^-1 preserves P T:Type, P:(TProp), R:(TTProp). (Sym x,y:T. x R y) R preserves P R^-1 preserves P x:A. B(x) Q
T